i1, i2, j1, j2:. (i1 < j1)  (i2  j2)  ((i1+i2) < (j1+j2)) 

latex

Up	int 2, int 2
Definitions	, t  T, P  Q, x:A. B(x), False, A, A  B, P  Q, P & Q, P  Q
Lemmas	le wf, lt to le, add functionality wrt le